#include "wdm.h"
#include "wdf.h"
#include "instrumentation.h"


// Introducing a dummy definition of the vararg WppAutoLogTrace function so
// that HAVOC drops calls to it
NTSTATUS
WppAutoLogTrace(
    IN PVOID              AutoLogContext,
    IN UCHAR              MessageLevel,
    IN ULONG              MessageFlags,
    IN LPGUID             MessageGuid,
    IN USHORT             MessageNumber,
    IN ...
    ) {}


// ****  WDM STUBS BEGIN  ****

// Interlocked operations
LONG
storm_InterlockedIncrement(
  IN LONG *Addend
  )
{
  LONG tmp;
  STORM_ATOMIC(
    (*Addend)++;
    tmp = *Addend;
  );
  return tmp;
}

LONG
storm_InterlockedDecrement(
  IN LONG *Addend
  )
{
  LONG tmp;
  STORM_ATOMIC(
    (*Addend)--;
    tmp = *Addend;
  );
  return tmp;
}

LONG
storm_InterlockedCompareExchange(
  __inout LONG volatile *Destination,
  __in LONG ExChange,
  __in LONG Comperand
  )
{
  LONG tmp;
  STORM_ATOMIC(
    tmp = *Destination;
    if (*Destination == Comperand) {
      *Destination = ExChange;
    }
  );
  return tmp;
}

PLIST_ENTRY
storm_ExInterlockedRemoveHeadList(
  IN PLIST_ENTRY ListHead,
  IN PKSPIN_LOCK Lock
  )
{
  PLIST_ENTRY returnVal;
  KIRQL irql;
  storm_KeAcquireSpinLock(Lock, &irql);
  returnVal = RemoveHeadList(ListHead);
  storm_KeReleaseSpinLock(Lock, irql);
  if (returnVal == ListHead) {
    returnVal = NULL;
  }
  return returnVal;
}

PLIST_ENTRY
storm_ExInterlockedInsertHeadList(
  IN PLIST_ENTRY ListHead,
  IN PLIST_ENTRY ListEntry,
  IN PKSPIN_LOCK Lock
  )
{
  PLIST_ENTRY returnVal;
  KIRQL irql;
  storm_KeAcquireSpinLock(Lock, &irql);
  returnVal = ListHead->Flink;
  InsertHeadList(ListHead, ListEntry);
  storm_KeReleaseSpinLock(Lock, irql);
  if (returnVal == ListHead) {
    returnVal = NULL;
  }
  return returnVal;
}

PLIST_ENTRY
storm_ExInterlockedInsertTailList(
  IN PLIST_ENTRY ListHead,
  IN PLIST_ENTRY ListEntry,
  IN PKSPIN_LOCK Lock
  )
{
  PLIST_ENTRY returnVal;
  KIRQL irql;
  storm_KeAcquireSpinLock(Lock, &irql);
  returnVal = ListHead->Blink;
  InsertTailList(ListHead, ListEntry);
  storm_KeReleaseSpinLock(Lock, irql);
  if (returnVal == ListHead) {
    returnVal = NULL;
  }
  return returnVal;
}


// Spinlocks
VOID
storm_KeInitializeSpinLock(
  IN PKSPIN_LOCK SpinLock
  )
{
  __hv_updates_resource("LOCK", SpinLock, UNLOCKED);
}

VOID
storm_KeAcquireSpinLock(
  IN PKSPIN_LOCK SpinLock,
  OUT PKIRQL OldIrql
  )
{
  int tid = storm_getThreadID();
  int lockStatus;
  STORM_ATOMIC(
    __hv_assume(__resource("LOCK", SpinLock) == lockStatus);
    STORM_ASSERT(tid != lockStatus);
    __hv_assume(lockStatus == UNLOCKED);
    __hv_updates_resource("LOCK", SpinLock, tid);
  );
}

VOID
storm_KeReleaseSpinLock(
  IN PKSPIN_LOCK SpinLock,
  IN KIRQL NewIrql
  )
{
  int lockStatus;
  STORM_ATOMIC(
    __hv_assume(__resource("LOCK", SpinLock) == lockStatus);
    STORM_ASSERT(lockStatus == storm_getThreadID());
    __hv_updates_resource("LOCK", SpinLock, UNLOCKED);
  );
}

VOID
storm_KeAcquireSpinLockAtDpcLevel(
  IN PKSPIN_LOCK SpinLock
  )
{
  int tid = storm_getThreadID();
  int lockStatus;
  STORM_ATOMIC(
    __hv_assume(__resource("LOCK", SpinLock) == lockStatus);
    STORM_ASSERT(tid != lockStatus);
    __hv_assume(lockStatus == UNLOCKED);
    __hv_updates_resource("LOCK", SpinLock, tid);
  );
}

VOID
storm_KeReleaseSpinLockFromDpcLevel(
  IN PKSPIN_LOCK SpinLock
  )
{
  int lockStatus;
  STORM_ATOMIC(
    __hv_assume(__resource("LOCK", SpinLock) == lockStatus);
    STORM_ASSERT(lockStatus == storm_getThreadID());
    __hv_updates_resource("LOCK", SpinLock, UNLOCKED);
  );
}

VOID
storm_IoAcquireCancelSpinLock(
  __out PKIRQL Irql
  )
{
  int tid = storm_getThreadID();
  STORM_ATOMIC(
    STORM_ASSERT(tid != cancelLockStatus);
    __hv_assume(cancelLockStatus == UNLOCKED);
    cancelLockStatus = tid;
  );
}

VOID
storm_IoReleaseCancelSpinLock(
  __in KIRQL Irql
  )
{
  STORM_ATOMIC(
    STORM_ASSERT(cancelLockStatus == storm_getThreadID());
    cancelLockStatus = UNLOCKED;
  );
}

NTSTATUS
storm_IoAcquireRemoveLock(
  IN PIO_REMOVE_LOCK RemoveLock,
  IN OPTIONAL PVOID Tag
  )
{
  NTSTATUS status;

  if (storm_nondet()) {
    status = STATUS_SUCCESS;
  } else {
    __hv_assume(!NT_SUCCESS(status));
  }

  return status;
}


// Events, semaphores
VOID
storm_KeInitializeEvent(
  IN PRKEVENT Event,
  IN EVENT_TYPE Type,
  IN BOOLEAN State
  )
{
  __hv_updates_resource("EVENT", Event, State);
}

LONG
storm_KeSetEvent(
  IN PRKEVENT Event,
  IN KPRIORITY Increment,
  IN BOOLEAN Wait
  )
{
  __hv_updates_resource("EVENT", Event, 1);
}

LONG
storm_KeResetEvent(
  IN PRKEVENT Event
  )
{
  LONG eventState;

  STORM_ATOMIC(
    __hv_assume(__resource("EVENT", Event) == eventState);
    __hv_updates_resource("EVENT", Event, 0);
  );

  return eventState;
}

VOID
storm_KeClearEvent(
  IN PRKEVENT Event
  )
{
  __hv_updates_resource("EVENT", Event, 0);
}

VOID
storm_KeInitializeSemaphore(
  IN PRKSEMAPHORE Semaphore,
  IN LONG Count,
  IN LONG Limit
  )
{
  __hv_updates_resource("EVENT", Semaphore, Count);
}

LONG
storm_KeReleaseSemaphore(
  IN PRKSEMAPHORE Semaphore,
  IN KPRIORITY Increment,
  IN LONG Adjustment,
  IN BOOLEAN Wait
  )
{
  LONG semaphoreState, oldSemaphoreState;

  STORM_ATOMIC(
    __hv_assume(__resource("EVENT", Semaphore) == semaphoreState);
    oldSemaphoreState = semaphoreState;
    semaphoreState += Adjustment;
    __hv_updates_resource("EVENT", Semaphore, semaphoreState);
  );

  return oldSemaphoreState;
}

NTSTATUS
storm_KeWaitForSingleObject(
  IN PVOID Object,
  IN KWAIT_REASON WaitReason,
  IN KPROCESSOR_MODE WaitMode,
  IN BOOLEAN Alertable,
  IN PLARGE_INTEGER Timeout OPTIONAL
  )
{
  LONG eventState;
  NTSTATUS status;

  STORM_ATOMIC(
    if (Timeout == NULL) {
      // Wait indefinitely
      __hv_assume(__resource("EVENT", Object) == eventState);
      __hv_assume(0 < eventState);
      eventState--;
      __hv_updates_resource("EVENT", Object, eventState);
      status = STATUS_SUCCESS;
    } else {
      if (storm_nondet()) {
        // Success
        __hv_assume(__resource("EVENT", Object) == eventState);
        __hv_assume(0 < eventState);
        eventState--;
        __hv_updates_resource("EVENT", Object, eventState);
        status = STATUS_SUCCESS;
      } else {
        // Timeout
        __hv_assume(__resource("EVENT", Object) <= 0);
        status = STATUS_TIMEOUT;
      }
    }
  );

  return status;
}


// Device operations
NTSTATUS
storm_IoCreateDevice(
  IN PDRIVER_OBJECT DriverObject,
  IN ULONG DeviceExtensionSize,
  IN PUNICODE_STRING DeviceName OPTIONAL,
  IN DEVICE_TYPE DeviceType,
  IN ULONG DeviceCharacteristics,
  IN BOOLEAN Exclusive,
  OUT PDEVICE_OBJECT *DeviceObject
  )
{
  NTSTATUS status;
  PVOID deviceExtension;
  PDEVICE_OBJECT deviceObject;

  if (storm_nondet()) {
    deviceObject = (PDEVICE_OBJECT)malloc(sizeof(DEVICE_OBJECT));
    deviceExtension = malloc(DeviceExtensionSize);
    deviceObject->DeviceExtension = deviceExtension;
    *DeviceObject = deviceObject;
    status = STATUS_SUCCESS;
  } else {
    __hv_assume(!NT_SUCCESS(status));
  }
  return status; 
}

PDEVICE_OBJECT
storm_IoAttachDeviceToDeviceStack(
  IN PDEVICE_OBJECT SourceDevice,
  IN PDEVICE_OBJECT TargetDevice
  )
{
  TargetDevice->AttachedDevice = SourceDevice;
  if (storm_nondet()) {
    return TargetDevice;
  } else {
    return NULL;
  }
}


// IRP operations
PIRP
storm_IoAllocateIrp(
  IN CCHAR StackSize,
  IN BOOLEAN ChargeQuota
  )
{
  PIRP createdIrp;
  PIO_STACK_LOCATION irpSp;
  switch (storm_nondet()) {
    case 0:
      STORM_ATOMIC(
        createdIrp = (PIRP)malloc(sizeof(IRP));
        createdIrp->Cancel = FALSE;
        createdIrp->CancelRoutine = NULL;
        __hv_updates_resource("COMPLETED", createdIrp, FALSE);

        __hv_assume(0 < StackSize);
        irpSp = (PIO_STACK_LOCATION)malloc(StackSize*sizeof(IO_STACK_LOCATION));
        createdIrp->Tail.Overlay.CurrentStackLocation = irpSp + StackSize;
        irpSp = IoGetNextIrpStackLocation(createdIrp);
        irpSp->CompletionRoutine = NULL;
        irpSp->Context = NULL;
      );
      break;

    default:
      // allocation can fail
      createdIrp = NULL;
  }
  return createdIrp;
}

PIRP
storm_IoBuildDeviceIoControlRequest(
  IN ULONG IoControlCode,
  IN PDEVICE_OBJECT DeviceObject,
  IN PVOID InputBuffer OPTIONAL,
  IN ULONG InputBufferLength,
  OUT PVOID OutputBuffer OPTIONAL,
  IN ULONG OutputBufferLength,
  IN BOOLEAN InternalDeviceIoControl,
  IN PKEVENT Event,
  OUT PIO_STATUS_BLOCK IoStatusBlock
  )
{
  PIRP createdIrp;
  createdIrp = storm_IoAllocateIrp(2, FALSE);
  if (createdIrp != NULL) {
    PIO_STACK_LOCATION irpSp = IoGetNextIrpStackLocation(createdIrp);
    irpSp->DeviceObject = DeviceObject;
  }
  return createdIrp;
}

VOID
storm_IoFreeIrp(
  IN PIRP pirp
  )
{
  COMPLETED_CHECK(pirp);
  __hv_updates_resource("COMPLETED", pirp, TRUE);
}

VOID
storm_IoCompleteRequest(
  IN PIRP pirp,
  IN CCHAR PriorityBoost
  )
{
  COMPLETED_CHECK(pirp);
  __hv_updates_resource("COMPLETED", pirp, TRUE);
}

BOOLEAN
storm_IoCancelIrp(
  IN PIRP Irp
  )
{
  PDRIVER_CANCEL oldCancelRoutine;

  // set Cancel flag
  Irp->Cancel = TRUE;

  STORM_ATOMIC(
    oldCancelRoutine = Irp->CancelRoutine;
    Irp->CancelRoutine = NULL;
  );

  storm_IoAcquireCancelSpinLock(&Irp->CancelIrql);
  if (oldCancelRoutine != NULL) {
    PIO_STACK_LOCATION irpSp;
    irpSp = IoGetCurrentIrpStackLocation(Irp);
    oldCancelRoutine(irpSp->DeviceObject, Irp);
    return TRUE;
  } else {
    return FALSE;
  }
}

VOID
storm_IoMarkIrpPending(
  IN OUT PIRP pirp
  )
{
  COMPLETED_CHECK(pirp);
}


// Setting cancel and complete routines
PDRIVER_CANCEL
storm_IoSetCancelRoutine(
  IN PIRP pirp,
  IN PDRIVER_CANCEL CancelRoutine
  )
{
  PDRIVER_CANCEL oldCancelRoutine;
  COMPLETED_CHECK(pirp);
  STORM_ATOMIC(
    oldCancelRoutine = pirp->CancelRoutine;
    pirp->CancelRoutine = CancelRoutine;
  );
  return oldCancelRoutine;
}

VOID
storm_IoSetCompletionRoutine(
  IN PIRP pirp,
  IN PIO_COMPLETION_ROUTINE CompletionRoutine,
  IN PVOID Context,
  IN BOOLEAN InvokeOnSuccess,
  IN BOOLEAN InvokeOnError,
  IN BOOLEAN InvokeOnCancel
  )
{
  PIO_STACK_LOCATION irpSp;
  COMPLETED_CHECK(pirp);
  irpSp = IoGetNextIrpStackLocation(pirp);
  irpSp->CompletionRoutine = CompletionRoutine;
  irpSp->Context = Context;
}

NTSTATUS
storm_IoSetCompletionRoutineEx(
  IN PDEVICE_OBJECT DeviceObject,
  IN PIRP Irp,
  IN PIO_COMPLETION_ROUTINE CompletionRoutine,
  IN PVOID Context,
  IN BOOLEAN InvokeOnSuccess,
  IN BOOLEAN InvokeOnError,
  IN BOOLEAN InvokeOnCancel
  )
{
  PIO_STACK_LOCATION irpSp;
  COMPLETED_CHECK(Irp);
  switch (storm_nondet()) {
    case 0: 
      storm_IoSetCompletionRoutine(Irp, CompletionRoutine,
        Context, InvokeOnSuccess, InvokeOnError, InvokeOnCancel);
      return STATUS_SUCCESS;
    default:
      return STATUS_INSUFFICIENT_RESOURCES;
  }
}

void CallCompletionRoutine(PIRP Irp) {
  PVOID context;
  PIO_STACK_LOCATION irpSp;
  PIO_COMPLETION_ROUTINE completionRoutine;
  NTSTATUS status;

  irpSp = IoGetCurrentIrpStackLocation(Irp);
  completionRoutine = irpSp->CompletionRoutine;
  context = irpSp->Context;
  Irp->Tail.Overlay.CurrentStackLocation++;
  irpSp = IoGetCurrentIrpStackLocation(Irp);
  
  if (completionRoutine != NULL) {
    __hv_updates_resource("COMPLETED", Irp, FALSE);
    status = completionRoutine(irpSp->DeviceObject, Irp, context);
    if (status != STATUS_MORE_PROCESSING_REQUIRED) {
      __hv_updates_resource("COMPLETED", Irp, TRUE);
    }
  }
}

NTSTATUS
storm_IoCallDriver(
  IN PDEVICE_OBJECT DeviceObject,
  IN OUT PIRP Irp
  )
{
  NTSTATUS compRetStatus;
  NTSTATUS status;
  PIO_STACK_LOCATION irpSp;

  COMPLETED_CHECK(Irp);

  IoSetNextIrpStackLocation(Irp);
  irpSp = IoGetCurrentIrpStackLocation(Irp);
  irpSp->DeviceObject = DeviceObject;
  __hv_updates_resource("COMPLETED", Irp, TRUE);

  if (storm_nondet()) {
    // sync call
    if (storm_nondet()) {
      Irp->IoStatus.Status = status = STATUS_SUCCESS;
      Irp->PendingReturned = 0;
    } else {
      Irp->IoStatus.Status = status = STATUS_UNSUCCESSFUL;
      Irp->PendingReturned = 0;
    }
    CallCompletionRoutine(Irp);
  } else {
    // async call
    status = STATUS_PENDING;
    Irp->PendingReturned = 1;
    __async_call CallCompletionRoutine(Irp);
  }

  return status;
}

NTSTATUS
storm_PoCallDriver(
  IN PDEVICE_OBJECT DeviceObject,
  IN OUT PIRP Irp
  )
{
  return storm_IoCallDriver(DeviceObject, Irp);
}


// Utils
PVOID
storm_ExAllocatePoolWithTag(
  IN POOL_TYPE PoolType,
  IN SIZE_T NumberOfBytes,
  IN ULONG Tag
  )
{
  return malloc(NumberOfBytes);
}

// ****  WDM STUBS END  ****



// ****  WDF STUBS BEGIN  ****

NTSTATUS
storm_SetReturnStatus()
{
  switch(storm_nondet()) {
    case 0:
      return (NTSTATUS) STATUS_NOT_SUPPORTED;
    default:
      return (NTSTATUS) STATUS_SUCCESS;
  }
}

// Reference counting
VOID
storm_WdfObjectReference(
  IN WDFOBJECT Handle
  )
{
  int count;
  STORM_ATOMIC(
    __hv_assume(__resource("REFERENCE", Handle) == count);
    count++;
    __hv_updates_resource("REFERENCE", Handle, count);
  );
}

VOID
storm_WdfObjectDereference(
  IN WDFOBJECT Handle
  )
{
  int count;
  STORM_ATOMIC(
    __hv_assume(__resource("REFERENCE", Handle) == count);
    count--;
    __hv_updates_resource("REFERENCE", Handle, count);
  );
}


// Spinlocks
NTSTATUS
storm_WdfSpinLockCreate(
  PWDF_OBJECT_ATTRIBUTES SpinLockAttributes,
  WDFSPINLOCK* SpinLock
  )
{
  if (storm_nondet()) {
    WDFSPINLOCK newLock = (WDFSPINLOCK)malloc(sizeof(WDFSPINLOCK));
    STORM_ATOMIC(
      __hv_updates_resource("LOCK", newLock, UNLOCKED);
      *SpinLock = newLock;
    );
    return STATUS_SUCCESS;
  } else {
    NTSTATUS status;
    __hv_assume(!NT_SUCCESS(status));
    return status;
  }
}

VOID
storm_WdfSpinLockAcquire(
  WDFSPINLOCK SpinLock
  )
{
  int tid = storm_getThreadID();
  int lockStatus;
  STORM_ATOMIC(
    __hv_assume(__resource("LOCK", SpinLock) == lockStatus);
    STORM_ASSERT(tid != lockStatus);
    __hv_assume(lockStatus == UNLOCKED);
    __hv_updates_resource("LOCK", SpinLock, tid);
  );
}

VOID
storm_WdfSpinLockRelease(
  WDFSPINLOCK SpinLock
  )
{
  int lockStatus;
  STORM_ATOMIC(
    __hv_assume(__resource("LOCK", SpinLock) == lockStatus);
    STORM_ASSERT(lockStatus == storm_getThreadID());
    __hv_updates_resource("LOCK", SpinLock, UNLOCKED);
  );
}


// WDFREQUEST operations
NTSTATUS
storm_WdfRequestCreate(
  IN OPTIONAL PWDF_OBJECT_ATTRIBUTES RequestAttributes,
  IN OPTIONAL WDFIOTARGET IoTarget,
  OUT WDFREQUEST* Request
  )
{
  PVOID Context;
  STORM_ATOMIC(
    *Request = (WDFREQUEST)malloc(sizeof(WDFREQUEST));
    Context = malloc(200);
    __hv_assume(__resource("COMPLETED", *Request) == FALSE);
    __hv_assume(__resource("CANCEL_ROUTINE", *Request) == NULL);
    __hv_assume(__resource("CANCEL_STARTED", *Request) == FALSE);
    __hv_assume(__resource("COMPLETION_ROUTINE", *Request) == NULL);
    __hv_assume(__resource("COMPLETION_CONTEXT", *Request) == NULL);
    __hv_assume(__resource("SENT", *Request) == FALSE);
    __hv_assume(__resource("COLLECTION", *Request) == NULL);
    __hv_assume(__resource("REFERENCE", *Request) == 0);
    __hv_assume(__resource("CONTEXT", *Request) == Context);
    __hv_assume(__resource("OBJECT", Context) == *Request);
    if (storm_nondet()) {
      __hv_assume(*Request == &created_hrequest);
      __hv_assume(Context == &created_hrctx);
    }
  )
  return storm_SetReturnStatus();
}

NTSTATUS
storm_WdfObjectCreate(
  IN OPTIONAL PWDF_OBJECT_ATTRIBUTES Attributes,
  OUT WDFOBJECT* Object
  )
{
  *Object = (WDFOBJECT)malloc(sizeof(WDFOBJECT));
  __hv_assume(*Object != &created_hrequest);
  return storm_SetReturnStatus();  
}

VOID
storm_WdfObjectDelete(
  WDFOBJECT Object
  )
{
  if (Object == &hrequest) {
    COMPLETED_CHECK(Object);
  } else if (Object == &created_hrequest) {
    COMPLETED_CHECK(Object);
  }
  STORM_ATOMIC(
    __hv_assume(__resource("REFERENCE", Object) == 0);
    __hv_updates_resource("COMPLETED", Object, TRUE);
    __hv_updates_resource("CANCEL_ROUTINE", Object, NULL);
  );
}

BOOLEAN
storm_WdfRequestIsCanceled(
  IN WDFREQUEST Request
  )
{
  COMPLETED_CHECK(Request);
	return (BOOLEAN)storm_nondet();
}

BOOLEAN
storm_WdfRequestCancelSentRequest(
  IN WDFREQUEST Request
  )
{
  COMPLETED_CHECK(Request);
  return (BOOLEAN)storm_nondet();
}

BOOLEAN
storm_WdfRequestSend(
  WDFREQUEST Request,
  WDFIOTARGET Target,
  PWDF_REQUEST_SEND_OPTIONS RequestOptions
  )
{
  BOOLEAN retVal = (BOOLEAN)storm_nondet();
  COMPLETED_CHECK(Request);
  if (retVal) {
    __hv_updates_resource("SENT", Request, TRUE);
  }
  return retVal;
}

NTSTATUS
storm_WdfRequestGetStatus(
  WDFREQUEST Request
  )
{
  COMPLETED_CHECK(Request);
	return storm_SetReturnStatus();
}

VOID
storm_WdfRequestGetParameters(
  IN WDFREQUEST Request,
  OUT PWDF_REQUEST_PARAMETERS Parameters
  )
{
  COMPLETED_CHECK(Request);
	Parameters = (PWDF_REQUEST_PARAMETERS)malloc(sizeof(WDF_REQUEST_PARAMETERS));
}

WDFFILEOBJECT
storm_WdfRequestGetFileObject(
  IN WDFREQUEST Request
  )
{
  COMPLETED_CHECK(Request);
  return (WDFFILEOBJECT)&notused_4hfileobj;
}

VOID
storm_WdfRequestComplete(
  IN WDFREQUEST Request,
  IN NTSTATUS RequestStatus
  )
{
  COMPLETED_CHECK(Request);
  STORM_ATOMIC(
    __hv_assume(__resource("REFERENCE", Request) == 0);
    __hv_updates_resource("COMPLETED", Request, TRUE);
    __hv_updates_resource("CANCEL_ROUTINE", Request, NULL);
  );
}

VOID
storm_WdfRequestCompleteWithInformation(
  WDFREQUEST Request,
  NTSTATUS RequestStatus,
  ULONG_PTR Information
  )
{
  COMPLETED_CHECK(Request);
  STORM_ATOMIC(
    __hv_assume(__resource("REFERENCE", Request) == 0);
    __hv_updates_resource("COMPLETED", Request, TRUE);
    __hv_updates_resource("CANCEL_ROUTINE", Request, NULL);
  );
}

VOID
storm_WdfRequestCompleteWithPriorityBoost(
  IN WDFREQUEST Request,
  IN NTSTATUS Status,
  IN CCHAR PriorityBoost
  )
{
  COMPLETED_CHECK(Request);
  STORM_ATOMIC(
    __hv_assume(__resource("REFERENCE", Request) == 0);
    __hv_updates_resource("COMPLETED", Request, TRUE);
    __hv_updates_resource("CANCEL_ROUTINE", Request, NULL);
  );
}


// Setting cancel and complete routines
VOID
storm_WdfRequestMarkCancelable(
  IN WDFREQUEST Request,
  IN PFN_WDF_REQUEST_CANCEL EvtRequestCancel
  )
{
  COMPLETED_CHECK(Request);
  __hv_updates_resource("CANCEL_ROUTINE", Request, EvtRequestCancel);
}

NTSTATUS
storm_WdfRequestMarkCancelableEx(
  IN WDFREQUEST Request,
  IN PFN_WDF_REQUEST_CANCEL EvtRequestCancel
  )
{
  LONG choice = (LONG)storm_nondet();

  COMPLETED_CHECK(Request);
  STORM_ATOMIC(
    if (storm_nondet()) {
      __hv_assume(__resource("CANCEL_STARTED", Request) == FALSE);
      __hv_assume(__resource("CANCEL_ROUTINE", Request) == NULL);
      __hv_updates_resource("CANCEL_ROUTINE", Request, EvtRequestCancel);
      choice = 0;
    } else {
      __hv_assume(__resource("CANCEL_STARTED", Request) == TRUE);
      choice = 1;
    }
  );

  switch (choice) {
    case 0:
      return (NTSTATUS) STATUS_SUCCESS;
      break;
    case 1:
      return (NTSTATUS) STATUS_CANCELLED;
      break;
    default:
      return (NTSTATUS) STATUS_INVALID_DEVICE_REQUEST;
      break;
  }
}

NTSTATUS
storm_WdfRequestUnmarkCancelable(
  IN WDFREQUEST Request
  )
{
  LONG choice = (LONG)storm_nondet();

  COMPLETED_CHECK(Request);
  STORM_ATOMIC(
    if (storm_nondet()) {
      __hv_assume(__resource("CANCEL_STARTED", Request) == TRUE);
      choice = 1;
    } else {
      __hv_assume(__resource("CANCEL_STARTED", Request) == FALSE);
    }
    __hv_updates_resource("CANCEL_ROUTINE", Request, NULL);
  );

  switch (choice) {
    case 0:
      return (NTSTATUS) STATUS_NOT_SUPPORTED;
      break;
    case 1:
      return (NTSTATUS) STATUS_CANCELLED;
      break;
    default:
      return (NTSTATUS) STATUS_SUCCESS;
      break;
  }
}

VOID
storm_WdfRequestSetCompletionRoutine(
  WDFREQUEST Request,
  PFN_WDF_REQUEST_COMPLETION_ROUTINE CompletionRoutine,
  WDFCONTEXT CompletionContext
  )
{
  COMPLETED_CHECK(Request);
  STORM_ATOMIC(
    __hv_updates_resource("COMPLETION_ROUTINE", Request, CompletionRoutine);
    __hv_updates_resource("COMPLETION_CONTEXT", Request, CompletionContext);
  );
}


// Collection
NTSTATUS
storm_WdfCollectionCreate(
  PWDF_OBJECT_ATTRIBUTES CollectionAttributes,
  WDFCOLLECTION *Collection
  )
{
  if (storm_nondet()) {
    *Collection = (WDFCOLLECTION)malloc(1);
    return STATUS_SUCCESS;
  } else {
    NTSTATUS status;
    __hv_assume(!NT_SUCCESS(status));
    return status;
  }
}

WDFOBJECT
storm_WdfCollectionGetItem(
  IN WDFCOLLECTION Collection,
  IN ULONG Index
  )
{
  WDFREQUEST Request;
  PVOID Context;
  switch (storm_nondet()) {
    case 0:
      __hv_assume(__resource("COLLECTION", &hrequest) == Collection);
      return ((WDFOBJECT) &hrequest);
    case 1:
      __hv_assume(__resource("COLLECTION", &created_hrequest) == Collection);
      return ((WDFOBJECT) &created_hrequest);
    default: // return some random element
      STORM_ATOMIC(
        __hv_assume(__resource("COLLECTION", &hrequest) == NULL);
        __hv_assume(__resource("COLLECTION", &created_hrequest) == NULL);
        Request = (WDFREQUEST)malloc(sizeof(WDFREQUEST));
        Context = malloc(200);
        __hv_assume(__resource("COMPLETED", Request) == FALSE);
        __hv_assume(__resource("CANCEL_ROUTINE", Request) == NULL);
        __hv_assume(__resource("CANCEL_STARTED", Request) == FALSE);
        __hv_assume(__resource("COMPLETION_ROUTINE", Request) == NULL);
        __hv_assume(__resource("COMPLETION_CONTEXT", Request) == NULL);
        __hv_assume(__resource("SENT", Request) == FALSE);
        __hv_assume(__resource("COLLECTION", Request) == Collection);
        __hv_assume(__resource("REFERENCE", Request) == 0);
        __hv_assume(__resource("CONTEXT", Request) == Context);
        __hv_assume(__resource("OBJECT", Context) == Request);
      );
      return Request;
  }
}

WDFOBJECT
storm_WdfCollectionGetFirstItem(
  IN WDFCOLLECTION Collection
  )
{
  return WdfCollectionGetItem(Collection, 0);
}

NTSTATUS
storm_WdfCollectionAdd(
  WDFCOLLECTION Collection,
  WDFOBJECT Object
  )
{ 
  switch (storm_nondet()) {
    case 0:
      __hv_updates_resource("COLLECTION", Object, Collection);
      return STATUS_SUCCESS;
    default:
      return STATUS_UNSUCCESSFUL;
	}
}

VOID
storm_WdfCollectionRemove(
  WDFCOLLECTION Collection,
  WDFOBJECT Item
  )
{
  __hv_updates_resource("COLLECTION", Item, NULL);
}

ULONG
storm_WdfCollectionGetCount(
  WDFCOLLECTION Collection
  )
{
  return (ULONG)storm_nondet();
}


// WdmMdl
NTSTATUS
storm_WdfRequestRetrieveInputWdmMdl(
  IN WDFREQUEST Request,
  OUT PMDL* Mdl
  )
{
  COMPLETED_CHECK(Request);

  switch (storm_nondet()) {
    case 0:
      *Mdl = (PMDL)malloc(sizeof(MDL));
      return STATUS_SUCCESS;
    default:
      *Mdl = (PMDL)malloc(sizeof(MDL));
      return STATUS_NOT_SUPPORTED;
  }
}

NTSTATUS
storm_WdfRequestRetrieveOutputWdmMdl(
  IN WDFREQUEST Request,
  OUT PMDL* Mdl
  )
{
  COMPLETED_CHECK(Request);

  switch (storm_nondet()) {
    case 0:
      *Mdl = (PMDL)malloc(sizeof(MDL));
      return STATUS_SUCCESS;
    default:
      *Mdl = (PMDL)malloc(sizeof(MDL));
      return STATUS_NOT_SUPPORTED;
  }
}


// Buffers
NTSTATUS
storm_WdfRequestRetrieveInputBuffer(
  IN WDFREQUEST Request,
  IN size_t  MinimumRequiredSize,
  OUT PVOID* Buffer,
  OUT size_t* Length
  )
{
  COMPLETED_CHECK(Request);

  Length = (size_t*)malloc(sizeof(size_t));
  switch (storm_nondet()) {
    case 0:
//      *Buffer = (PVOID)malloc(1);
      *Buffer = (PVOID)&hbuffer;
      return STATUS_SUCCESS;
    default: 
//      *Buffer = (PVOID)malloc(1);
      *Buffer = (PVOID)&hbuffer;
      return STATUS_UNSUCCESSFUL;
  }
}

NTSTATUS
storm_WdfRequestRetrieveOutputBuffer(
  IN WDFREQUEST Request,
  IN size_t  MinimumRequiredSize,
  OUT PVOID* Buffer,
  OUT size_t* Length
  )
{
  COMPLETED_CHECK(Request);

  Length = (size_t*)malloc(sizeof(size_t));
  switch (storm_nondet()) {
    case 0:
      *Buffer = (PVOID)malloc(1);
      return STATUS_SUCCESS;
    default: 
      *Buffer = (PVOID)malloc(1);
      return STATUS_UNSUCCESSFUL;
  }
}

PVOID
storm_WdfMemoryGetBuffer(
  IN WDFMEMORY Memory,
  OUT OPTIONAL size_t* BufferSize
  )
{
	BufferSize = (size_t*)malloc(sizeof(size_t));
	return (PVOID)malloc(1);
}


// Device
NTSTATUS
storm_WdfDeviceCreate(
  IN OUT PWDFDEVICE_INIT* DeviceInit,
  IN OPTIONAL PWDF_OBJECT_ATTRIBUTES DeviceAttributes,
  OUT WDFDEVICE* Device
  )
{
  switch (storm_nondet()) {
    case 0:
      *Device = (WDFDEVICE)&hdevice;
      return STATUS_SUCCESS;
    default: 
      *Device = (WDFDEVICE)&hdevice;
      return STATUS_UNSUCCESSFUL;
  }
}


// Queue
WDFQUEUE
storm_WdfDeviceGetDefaultQueue(
  IN WDFDEVICE Device
  )
{
  return (WDFQUEUE)&hqueue;
}

NTSTATUS
storm_WdfIoQueueCreate(
  IN WDFDEVICE Device,
  IN PWDF_IO_QUEUE_CONFIG Config,
  IN OPTIONAL PWDF_OBJECT_ATTRIBUTES QueueAttributes,
  OUT WDFQUEUE* Queue
  )
{ 
  switch (storm_nondet()) {
    case 0:
      *Queue = (WDFQUEUE)&hqueue;
      return STATUS_SUCCESS;
    default: 
      *Queue = (WDFQUEUE)&hqueue;
      return STATUS_UNSUCCESSFUL;
  }
}

WDFDEVICE
storm_WdfIoQueueGetDevice(
  IN WDFQUEUE Queue
  )
{
  return (WDFDEVICE)&hdevice;
}

WDFQUEUE
storm_WdfRequestGetIoQueue(
  IN WDFREQUEST Request
  )
{
  COMPLETED_CHECK(Request);
  return (WDFQUEUE)&hqueue;
}


// Timer
WDFOBJECT
storm_WdfTimerGetParentObject(
  IN WDFTIMER Timer
  )
{
  return &hqueue;
}


// Pipe
VOID
storm_WdfUsbTargetPipeGetInformation(
  IN WDFUSBPIPE Pipe,
  OUT PWDF_USB_PIPE_INFORMATION PipeInformation
  )
{
  PipeInformation->PipeType = (WDF_USB_PIPE_TYPE)storm_nondet();
  PipeInformation->MaximumPacketSize = (ULONG)storm_nondet();
  PipeInformation->MaximumTransferSize = (ULONG)storm_nondet();
}


// Utils
PVOID
storm_WdfObjectGetTypedContextWorker(
  WDFOBJECT Handle,
  PCWDF_OBJECT_CONTEXT_TYPE_INFO TypeInfo
  )
{
  PVOID Context;
  if (Handle == &hrequest) {
    COMPLETED_CHECK(Handle);
  } else if (Handle == &created_hrequest) {
    COMPLETED_CHECK(Handle);
  }
  __hv_assume(__resource("CONTEXT", Handle) == Context);
  return Context;
}

WDFOBJECT
storm_WdfObjectContextGetObject(
  IN PVOID ContextPointer
  )
{
  WDFOBJECT Object;
  __hv_assume(__resource("OBJECT", ContextPointer) == Object);
  return Object;
}

NTSTATUS
storm_WdfMemoryCreate(
  IN OPTIONAL PWDF_OBJECT_ATTRIBUTES Attributes,
  IN POOL_TYPE PoolType,
  IN OPTIONAL ULONG PoolTag,
  IN size_t BufferSize,
  OUT WDFMEMORY* Memory,
  OUT OPTIONAL PVOID* Buffer
  )
{
  *Memory = (WDFMEMORY)malloc(1);
  return storm_SetReturnStatus();
}

VOID
storm_WDF_REQUEST_PARAMETERS_INIT(
  OUT PWDF_REQUEST_PARAMETERS Parameters
  )
{
  Parameters = (PWDF_REQUEST_PARAMETERS)malloc(sizeof(WDF_REQUEST_PARAMETERS));
}

// ****  WDF STUBS END  ****

